File #1: atoe-tcsD.tex
File #2: atoe-tcsJE.tex

Nonmatching lines (File "atoe-tcsD.tex"; Line 1:3; File "atoe-tcsJE.tex"; Line 1)
   1	\documentstyle{elsart}
   2	
   3	

   1	\documentclass{elsart}


Extra lines in 1st before 8 in 2nd (File "atoe-tcsD.tex"; Line 10; File "atoe-tcsJE.tex"; Line 8)
  10	


Nonmatching lines (File "atoe-tcsD.tex"; Line 123:126; File "atoe-tcsJE.tex"; Line 120:123)
 123	\newcommand{\ben}{\begin{enumerate}}
 124	\newcommand{\een}{\end{enumerate}}
 125	\newcommand{\bit}{\begin{itemize}}
 126	\newcommand{\eit}{\end{itemize}}

 120	\newcommand{\ben}{\begin{description}}
 121	\newcommand{\een}{\end{description}}
 122	\newcommand{\bit}{\begin{description}}
 123	\newcommand{\eit}{\end{description}}


Nonmatching lines (File "atoe-tcsD.tex"; Line 236:237; File "atoe-tcsJE.tex"; Line 233:234)
 236	\newcommand{\stab}{{\cal S}}
 237	\newcommand{\reg}{{\cal S}}

 233	\newcommand{\stab}{\mathcal{S}}
 234	\newcommand{\reg}{\mathcal{S}}


Nonmatching lines (File "atoe-tcsD.tex"; Line 240; File "atoe-tcsJE.tex"; Line 237)
 240	\newcommand{\fcC}{{\cal L}({\cal C})}

 237	\newcommand{\fcC}{\mathcal{L(C)}}


Nonmatching lines (File "atoe-tcsD.tex"; Line 247:248; File "atoe-tcsJE.tex"; Line 244:245)
 247	\newcommand{\calF}{{\cal F}}
 248	\newcommand{\calR}{{\cal R}}

 244	\newcommand{\calF}{\mathcal{F}}
 245	\newcommand{\calR}{\mathcal{R}}


Nonmatching lines (File "atoe-tcsD.tex"; Line 294; File "atoe-tcsJE.tex"; Line 291:292)
 294	different from both Maranget's labelling for orthogonal TRSs~\cite{[Mar91]} and

 291	different from both Maranget's labelling for orthogonal
 292	TRSs~\cite{[Mar91]} and


Nonmatching lines (File "atoe-tcsD.tex"; Line 331:333; File "atoe-tcsJE.tex"; Line 329:333)
 331	introduced in $s$, while other redexes of $s$ are considered \emph{residuals} of
 332	redexes in $t$, as specified by the residual relation.
 333	Further, the residual relation is generalized to all (many-step) reductions, and

 329	introduced in $s$, while other redexes of $s$ are considered
 330	\emph{residuals} of
 331	redexes in $t$, as specified by the residual relation.
 332	Further, the residual relation is generalized to all (many-step)
 333	reductions, and


Nonmatching lines (File "atoe-tcsD.tex"; Line 502:503; File "atoe-tcsJE.tex"; Line 502:503)
 502	theorem for regular stable sets $\stab$ in an SDRS $\cal R$, and demonstrate
 503	that if $\cal R$ is not stable, then the theorem fails. In

 502	theorem for regular stable sets $\stab$ in an SDRS $\calR$, and demonstrate
 503	that if $\calR$ is not stable, then the theorem fails. In


Nonmatching lines (File "atoe-tcsD.tex"; Line 613; File "atoe-tcsJE.tex"; Line 613)
 613	We call a DRS $\cal R$ \emph{stable} (SDRS) if

 613	We call a DRS $\calR$ \emph{stable} (SDRS) if


Nonmatching lines (File "atoe-tcsD.tex"; Line 651:652; File "atoe-tcsJE.tex"; Line 651:653)
 651	$\cal R$, \emph{L\'evy-equivalence} or
 652	\emph{permutation-equivalence} is defined as the smallest relation on co-initial

 651	$\calR$, \emph{L\'evy-equivalence} or
 652	\emph{permutation-equivalence} is defined as the smallest
 653	relation on co-initial


Nonmatching lines (File "atoe-tcsD.tex"; Line 712:713; File "atoe-tcsJE.tex"; Line 713:715)
 712	be sound!) \emph{Klop's commutative diagrams} can be used instead~\cite{[Kl.
 713	CRS]}. Klop's diagrams are constructed using developments rather than

 713	be sound!) \emph{Klop's commutative diagrams} can be used
 714	instead~\cite{[Kl.CRS]}. Klop's diagrams are constructed using
 715	developments rather than


Nonmatching lines (File "atoe-tcsD.tex"; Line 752; File "atoe-tcsJE.tex"; Line 754:755)
 752	\item  Let $u\in U\subts t$ and $P:t\doar o$. We call $P$ \emph{external}

 754	\item[\labelitemi]  Let $u\in U\subts t$ and $P:t\doar o$.
 755	We call $P$ \emph{external}


Nonmatching lines (File "atoe-tcsD.tex"; Line 756; File "atoe-tcsJE.tex"; Line 759)
 756	\item  Let $P:t_0\dored{P_i}t_i\red{u_i}t_{i+1}\doar t_n$

 759	\item[\labelitemi]  Let $P:t_0\dored{P_i}t_i\red{u_i}t_{i+1}\doar t_n$


Nonmatching lines (File "atoe-tcsD.tex"; Line 907; File "atoe-tcsJE.tex"; Line 910)
 907	stable DRS $\cal R$, an $\stab$-normal form of an

 910	stable DRS $\calR$, an $\stab$-normal form of an


Nonmatching lines (File "atoe-tcsD.tex"; Line 911; File "atoe-tcsJE.tex"; Line 914)
 911	stability for $\cal R$, this result breaks down.

 914	stability for $\calR$, this result breaks down.


Nonmatching lines (File "atoe-tcsD.tex"; Line 917; File "atoe-tcsJE.tex"; Line 920)
 917	Let $\stab$ be a set of terms in a DRS $\cal R$.

 920	Let $\stab$ be a set of terms in a DRS $\calR$.


Nonmatching lines (File "atoe-tcsD.tex"; Line 1012; File "atoe-tcsJE.tex"; Line 1015)
1012	Let terms in the DRS $\cal R$ be $t=I(I(x))$, $s=I(x)$, and $e=x$; redexes in

1015	Let terms in the DRS $\calR$ be $t=I(I(x))$, $s=I(x)$, and $e=x$; redexes in


Nonmatching lines (File "atoe-tcsD.tex"; Line 1021; File "atoe-tcsJE.tex"; Line 1024)
1021	Hypernormalization theorem (proved below) is not valid for $({\cal R},\stab)$

1024	Hypernormalization theorem (proved below) is not valid for $({\calR},\stab)$


Nonmatching lines (File "atoe-tcsD.tex"; Line 1030; File "atoe-tcsJE.tex"; Line 1033:1034)
1030	We call  $P:t_0\ar t_1\ar\ldots$  \emph{$\stab$-(un)needed} if it contracts only

1033	We call  $P:t_0\ar t_1\ar\ldots$  \emph{$\stab$-(un)needed} if it
1034	contracts only


Nonmatching lines (File "atoe-tcsD.tex"; Line 1041; File "atoe-tcsJE.tex"; Line 1045:1046)
1041	$\reg$ in an SDRS $\cal R$, transforms any finite or infinite reduction $P$ into

1045	$\reg$ in an SDRS $\calR$, transforms any finite or infinite reduction
1046	$P$ into


Nonmatching lines (File "atoe-tcsD.tex"; Line 1089; File "atoe-tcsJE.tex"; Line 1094:1095)
1089	\item[(1)] Since the transformation $K$ does not change the number of  $\reg$-needed

1094	\item[(1)] Since the transformation $K$ does not change the number of
1095	$\reg$-needed


Nonmatching lines (File "atoe-tcsD.tex"; Line 1110; File "atoe-tcsJE.tex"; Line 1116)
1110	Let $\reg$ be a regular stable set of terms in a DRS $\cal R$, and let

1116	Let $\reg$ be a regular stable set of terms in a DRS $\calR$, and let


Nonmatching lines (File "atoe-tcsD.tex"; Line 1156:1157; File "atoe-tcsJE.tex"; Line 1162:1163)
1156	 \dTo^{u=U_0}  &     & \dOnto^{U_1} &          & \dOnto^{U_2}&         &      \\
1157	s_0    &   \rOnto_{u_0/U_0}  &   s_1   &   \rOnto_{u_1/U_1}  &   s_2    &

1162	 \dTo^{u=U_0}  &     & \dOnto^{U_1} &          & \dOnto^{U_2}&         & \\
1163	s_0    &   \rOnto_{u_0/U_0}  &   s_1   &   \rOnto_{u_1/U_1}  &   s_2   &


Nonmatching lines (File "atoe-tcsD.tex"; Line 1171:1172; File "atoe-tcsJE.tex"; Line 1177:1178)
1171	terms in a stable DRS $\cal R$, and let $t\not\in \reg$ be a term in $\cal
1172	R$. Then

1177	terms in a stable DRS $\calR$, and let $t\not\in \reg$ be a term in $\calR$.
1178	Then


Nonmatching lines (File "atoe-tcsD.tex"; Line 1176; File "atoe-tcsJE.tex"; Line 1182:1183)
1176	\item[(2)] $t$ has an $\reg$-normal form  iff it does not possess a reduction in

1182	\item[(2)] $t$ has an $\reg$-normal form  iff it does not possess a
1183	reduction in


Nonmatching lines (File "atoe-tcsD.tex"; Line 1246; File "atoe-tcsJE.tex"; Line 1253)
1246	(DFS) is a triple $\calF =(\calR,\fami,\contr)$, where $\cal R$ is a DRS;

1253	(DFS) is a triple $\calF =(\calR,\fami,\contr)$, where $\calR$ is a DRS;


Nonmatching lines (File "atoe-tcsD.tex"; Line 1252; File "atoe-tcsJE.tex"; Line 1259:1260)
1252	\item[(1)]  For any co-initial reductions $P$ and $Q$, a redex $Qv$ in the final

1259	\item[(1)]  For any co-initial reductions $P$ and $Q$, a redex $Qv$
1260	in the final


Nonmatching lines (File "atoe-tcsD.tex"; Line 1265; File "atoe-tcsJE.tex"; Line 1273)
1265	\item[{\rm [initial]}] Let $u,v\subt t$ and $u\not= v$, in $\cal R$.

1273	\item[{\rm [initial]}] Let $u,v\subt t$ and $u\not= v$, in $\calR$.


Nonmatching lines (File "atoe-tcsD.tex"; Line 1286; File "atoe-tcsJE.tex"; Line 1294)
1286	${\cal F} =({\cal R},\fami)$.

1294	${\calF} =({\calR},\fami)$.


Nonmatching lines (File "atoe-tcsD.tex"; Line 1341; File "atoe-tcsJE.tex"; Line 1349)
1341	In any DFS ${\cal F}$:

1349	In any DFS ${\calF}$:


Nonmatching lines (File "atoe-tcsD.tex"; Line 1376; File "atoe-tcsJE.tex"; Line 1384)
1376	 Consider the ARS $\cal R$ given by the figure below,

1384	 Consider the ARS $\calR$ given by the figure below,


Nonmatching lines (File "atoe-tcsD.tex"; Line 1392; File "atoe-tcsJE.tex"; Line 1400)
1392	 are satisfied too. Note that the DRS $\cal R$ is stable.

1400	 are satisfied too. Note that the DRS $\calR$ is stable.


Nonmatching lines (File "atoe-tcsD.tex"; Line 1410; File "atoe-tcsJE.tex"; Line 1418)
1410	Any DFS ${\cal F}$ is a stable DRS.

1418	Any DFS ${\calF}$ is a stable DRS.


Nonmatching lines (File "atoe-tcsD.tex"; Line 1433; File "atoe-tcsJE.tex"; Line 1441)
1433	Consider the DRS $\cal R$ given by the figure below, where $w$ and $w'$

1441	Consider the DRS $\calR$ given by the figure below, where $w$ and $w'$


Nonmatching lines (File "atoe-tcsD.tex"; Line 1438; File "atoe-tcsJE.tex"; Line 1446)
1438	DRS $\cal R$ is not stable.

1446	DRS $\calR$ is not stable.


Nonmatching lines (File "atoe-tcsD.tex"; Line 1460; File "atoe-tcsJE.tex"; Line 1468)
1460	DFS ${\cal F}$. Then  $u'$ also is $\stab$-unneeded.

1468	DFS ${\calF}$. Then  $u'$ also is $\stab$-unneeded.


Nonmatching lines (File "atoe-tcsD.tex"; Line 1479; File "atoe-tcsJE.tex"; Line 1487)
1479	a DFS~$\cal F$, and let $t\not\in \stab$ be $\stab$-normalizable. Then

1487	a DFS~$\calF$, and let $t\not\in \stab$ be $\stab$-normalizable. Then


Nonmatching lines (File "atoe-tcsD.tex"; Line 1532; File "atoe-tcsJE.tex"; Line 1540)
1532	 Let $\stab$ be a stable set of terms in a DFS ${\cal F}$, and let

1540	 Let $\stab$ be a stable set of terms in a DFS ${\calF}$, and let


Nonmatching lines (File "atoe-tcsD.tex"; Line 1567:1568; File "atoe-tcsJE.tex"; Line 1575:1576)
1567	Let $\stab$ be a stable set of terms in a DFS ${\cal F}$, and let $t$ be an
1568	$\stab$-normalizable term in $\cal F$. Then any weakly $\stab$-needed

1575	Let $\stab$ be a stable set of terms in a DFS ${\calF}$, and let $t$ be an
1576	$\stab$-normalizable term in $\calF$. Then any weakly $\stab$-needed


Nonmatching lines (File "atoe-tcsD.tex"; Line 1605; File "atoe-tcsJE.tex"; Line 1613)
1605	in a DFS ${\cal F}$. Then any  $\stab$-needed

1613	in a DFS ${\calF}$. Then any  $\stab$-needed


Nonmatching lines (File "atoe-tcsD.tex"; Line 1641:1642; File "atoe-tcsJE.tex"; Line 1649:1650)
1641	Let $\stab$ be a stable set of terms in a DFS~${\cal F}$, and let $t$ be an
1642	$\stab$-normalizable term in $\cal F$. Then any  $\stab$-needed

1649	Let $\stab$ be a stable set of terms in a DFS~${\calF}$, and let $t$ be an
1650	$\stab$-normalizable term in $\calF$. Then any  $\stab$-needed


Nonmatching lines (File "atoe-tcsD.tex"; Line 1740:1741; File "atoe-tcsJE.tex"; Line 1748:1749)
1740	\begin{itemize}
1741	\item   Let $P:t\doar o$ and $u\subt t$, in a DRS.  We call $u$

1748	\bit
1749	\item[\labelitemi]   Let $P:t\doar o$ and $u\subt t$, in a DRS.  We call $u$


Nonmatching lines (File "atoe-tcsD.tex"; Line 1745; File "atoe-tcsJE.tex"; Line 1753)
1745	\item  We call $u$ \emph{$P$-needed} if there is no

1753	\item[\labelitemi]  We call $u$ \emph{$P$-needed} if there is no


Nonmatching lines (File "atoe-tcsD.tex"; Line 1752; File "atoe-tcsJE.tex"; Line 1760:1761)
1752	\item Let $Q:t\doar o$, $P:t\dored{P'}s\doar e$, and $u\subt s$. We

1760	\item[\labelitemi] Let $Q:t\doar o$, $P:t\dored{P'}s\doar e$,
1761	and $u\subt s$. We


Nonmatching lines (File "atoe-tcsD.tex"; Line 1758; File "atoe-tcsJE.tex"; Line 1767)
1758	\end{itemize}

1767	\eit


Nonmatching lines (File "atoe-tcsD.tex"; Line 2021; File "atoe-tcsJE.tex"; Line 2030)
2021	{}      &       & v\in e     &\rOnto_\emp & e\ni v &\rOnto_\emp     &e\ni v  \\

2030	{}      &       & v\in e     &\rOnto_\emp & e\ni v &\rOnto_\emp   &e\ni v \\


Nonmatching lines (File "atoe-tcsD.tex"; Line 2089; File "atoe-tcsJE.tex"; Line 2098)
2089	\cdot         &\rTo     & \cdot       &\rTo^{v'} & \cdot     &\rOnto      &\cdot  \\

2098	\cdot         &\rTo     & \cdot    &\rTo^{v'} & \cdot   &\rOnto   &\cdot  \\


Nonmatching lines (File "atoe-tcsD.tex"; Line 2094; File "atoe-tcsJE.tex"; Line 2103)
2094	Q          &\rTo_{u'}& Q'     &\rOnto_\emp & \cdot     &\rOnto      &\cdot  \\

2103	Q          &\rTo_{u'}& Q'     &\rOnto_\emp & \cdot     &\rOnto    &\cdot \\


Nonmatching lines (File "atoe-tcsD.tex"; Line 2346; File "atoe-tcsJE.tex"; Line 2355)
2346	\item[(1)] We call a DFS $\cal F$ a \emph{zig-zag} DFS, ZDFS, if its family

2355	\item[(1)] We call a DFS $\calF$ a \emph{zig-zag} DFS, ZDFS, if its family


Nonmatching lines (File "atoe-tcsD.tex"; Line 2449; File "atoe-tcsJE.tex"; Line 2458)
2449	Any reduction in an ASDRS $\cal R$ can contract at most one element of a

2458	Any reduction in an ASDRS $\calR$ can contract at most one element of a


Nonmatching lines (File "atoe-tcsD.tex"; Line 2453; File "atoe-tcsJE.tex"; Line 2462)
2453	Let $P:t_o\red{u_0}t_1\red{u_1}\ldots$ be a reduction in $\cal$, and let

2462	Let $P:t_o\red{u_0}t_1\red{u_1}\ldots$ be a reduction in $\calR$, and let


Nonmatching lines (File "atoe-tcsD.tex"; Line 2560:2561; File "atoe-tcsJE.tex"; Line 2569:2570)
2560	Let $\cal R$ be a non-duplicating SDRS. Then ${\cal
2561	F_R}=(R,\zfami,\zcontr)$ is a non-duplicating zig-zag DFS.

2569	Let $\calR$ be a non-duplicating SDRS. Then ${\calF_R}=(R,\zfami,\zcontr)$
2570	is a non-duplicating zig-zag DFS.


Nonmatching lines (File "atoe-tcsD.tex"; Line 2564; File "atoe-tcsJE.tex"; Line 2573)
2564	We need to show that ${\cal F_R}$ satisfies all family axioms.

2573	We need to show that ${\calF_R}$ satisfies all family axioms.


Nonmatching lines (File "atoe-tcsD.tex"; Line 2673:2674; File "atoe-tcsJE.tex"; Line 2682:2683)
2673	of separability of a DFS $\cal F$ via uniqueness of contracted families in
2674	reductions in $\cal F$. It shows that, in separable DFSs, and only in such

2682	of separability of a DFS $\calF$ via uniqueness of contracted families in
2683	reductions in $\calF$. It shows that, in separable DFSs, and only in such


Nonmatching lines (File "atoe-tcsD.tex"; Line 2679; File "atoe-tcsJE.tex"; Line 2688)
2679	Let ${\cal F}={\cal R}, \fami,\contr)$ be an affine DFS. Them the following

2688	Let ${\calF}={\calR}, \fami,\contr)$ be an affine DFS. Them the following


Nonmatching lines (File "atoe-tcsD.tex"; Line 2682; File "atoe-tcsJE.tex"; Line 2691)
2682	\item[(1)] $\cal F$ is separable;

2691	\item[(1)] $\calF$ is separable;


Nonmatching lines (File "atoe-tcsD.tex"; Line 2685; File "atoe-tcsJE.tex"; Line 2694)
2685	reduction in~$\cal F$;

2694	reduction in~$\calF$;


Nonmatching lines (File "atoe-tcsD.tex"; Line 2689; File "atoe-tcsJE.tex"; Line 2698)
2689	\item[(4)] Any reduction in $\cal F$ is in fact a complete

2698	\item[(4)] Any reduction in $\calF$ is in fact a complete


Nonmatching lines (File "atoe-tcsD.tex"; Line 2733; File "atoe-tcsJE.tex"; Line 2742)
2733	\item{$(4)\imply (1)$:} If $\cal F$ was not separable, then there would be $Pv$,

2742	\item{$(4)\imply (1)$:} If $\calF$ was not separable, then there would be $Pv$,


Nonmatching lines (File "atoe-tcsD.tex"; Line 2746:2747; File "atoe-tcsJE.tex"; Line 2755:2757)
2746	Let $Pv$ be a canonical element of a family $\phi$, in an affine DFS ${\cal
2747	F}=(R,\fami,\contr)$, and let $P$ contract a redex $w$. Then $Fam(w)\contr

2755	Let $Pv$ be a canonical element of a family $\phi$, in an affine DFS
2756	${\calF}=(R,\fami,\contr)$, and let $P$ contract a redex $w$. Then
2757	$Fam(w)\contr


Nonmatching lines (File "atoe-tcsD.tex"; Line 2769; File "atoe-tcsJE.tex"; Line 2779)
2769	An affine DFS $\cal F$ is separable iff it is a zig-zag DFS.

2779	An affine DFS $\calF$ is separable iff it is a zig-zag DFS.


Nonmatching lines (File "atoe-tcsD.tex"; Line 2773; File "atoe-tcsJE.tex"; Line 2783)
2773	\item[\suf] ${\cal F}=({\cal R}, \sfami,\scontr)$ be separable, and suppose

2783	\item[\suf] ${\calF}=({\calR}, \sfami,\scontr)$ be separable, and suppose


Nonmatching lines (File "atoe-tcsD.tex"; Line 2800:2801; File "atoe-tcsJE.tex"; Line 2810:2811)
2800	Let $Pv$ be a canonical element of a family $\phi$, in an AZDFS ${\cal
2801	F_R}=(R,\zfami,\zcontr)$. Then $P$ contracts exactly one redex

2810	Let $Pv$ be a canonical element of a family $\phi$, in an AZDFS
2811	${\calF_R}=(R,\zfami,\zcontr)$. Then $P$ contracts exactly one redex


Nonmatching lines (File "atoe-tcsD.tex"; Line 2816:2819; File "atoe-tcsJE.tex"; Line 2826:2829)
2816	We now define the \emph{implementation} $\lin{\cal F}$ of a DFS $\cal F$,
2817	whose reductions correspond to complete family-reductions in $\cal F$,
2818	hence the name. We also show that optimal reductions in $\cal F$, relative
2819	to any stable set $\stab$ of results, are implemented in $\lin{\cal F}$ by

2826	We now define the \emph{implementation} $\lin{\calF}$ of a DFS $\calF$,
2827	whose reductions correspond to complete family-reductions in $\calF$,
2828	hence the name. We also show that optimal reductions in $\calF$, relative
2829	to any stable set $\stab$ of results, are implemented in $\lin{\calF}$ by


Nonmatching lines (File "atoe-tcsD.tex"; Line 2828:2833; File "atoe-tcsJE.tex"; Line 2838:2844)
2828	Let ${\cal F}=({\cal R},\fami,\contr)$ be a DFS. The \emph{implementation}
2829	or \emph{L\'evy-implementation} of ${\cal F}$ is the AZDFS $\lin{{\cal
2830	F}}=({\cal R}_I,\fami_I,\contr_I)$, where
2831	\bit
2832	\item the branches of the reduction graph of the underlying ARS $A$ of
2833	${\cal R}_I=(A,/)$ are complete family-reductions starting from $t_\emp$,

2838	Let ${\calF}=({\calR},\fami,\contr)$ be a DFS. The \emph{implementation}
2839	or \emph{L\'evy-implementation} of ${\calF}$ is the AZDFS
2840	$\lin{{\calF}}=({\calR}_I,\fami_I,\contr_I)$, where
2841	\bit
2842	\item[\labelitemi] the branches of the reduction graph of the
2843	underlying ARS $A$ of
2844	${\calR}_I=(A,/)$ are complete family-reductions starting from $t_\emp$,


Nonmatching lines (File "atoe-tcsD.tex"; Line 2838; File "atoe-tcsJE.tex"; Line 2849:2850)
2838	\item the residual relation $/$ is defined as follows: let $U$ and $V$

2849	\item[\labelitemi] the residual relation $/$ is defined as follows:
2850	let $U$ and $V$


Nonmatching lines (File "atoe-tcsD.tex"; Line 2843:2844; File "atoe-tcsJE.tex"; Line 2855:2857)
2843	\item the family and contribution relations $\fami_I,\contr_I$ in
2844	$\lin{{\cal F}}$ are those induced by $\fami$ and $\contr:$ let $P_I$ and

2855	\item[\labelitemi] the family and contribution relations
2856	$\fami_I,\contr_I$ in
2857	$\lin{{\calF}}$ are those induced by $\fami$ and $\contr:$ let $P_I$ and


Nonmatching lines (File "atoe-tcsD.tex"; Line 2854; File "atoe-tcsJE.tex"; Line 2867)
2854	We need to verify that $\lin{{\cal F}}$ in the above definition is indeed

2867	We need to verify that $\lin{{\calF}}$ in the above definition is indeed


Nonmatching lines (File "atoe-tcsD.tex"; Line 2859; File "atoe-tcsJE.tex"; Line 2872)
2859	Let $P:t_\emp\doar s$ be a \cfr\ in a DFS ${\cal F}=(R,\fami,\contr)$,

2872	Let $P:t_\emp\doar s$ be a \cfr\ in a DFS ${\calF}=(R,\fami,\contr)$,


Nonmatching lines (File "atoe-tcsD.tex"; Line 2877:2878; File "atoe-tcsJE.tex"; Line 2890:2891)
2877	family in $s$. Further, [weak acyclicity] and [stability] for $\lin{{\cal
2878	F}}$ follow immediately from Acyclicity Lemma and Stability Lemma,

2890	family in $s$. Further, [weak acyclicity] and [stability] for $\lin{{\calF}}$
2891	follow immediately from Acyclicity Lemma and Stability Lemma,


Nonmatching lines (File "atoe-tcsD.tex"; Line 2881:2892; File "atoe-tcsJE.tex"; Line 2894:2905)
2881	clearly external). The axiom [initial] in $\lin{{\cal F}}$ follows
2882	immediately from [initial] in $\cal F$. If $P+U+V$ is a reduction in
2883	$\lin{{\cal F}}$ such that $U$ creates $V$, then the redexes in $V$ are
2884	created along $U$ (when $P+U+V$ is considered as a reduction in $\cal F$),
2885	i.e., $Fam(U)\contr Fam(V)$ in $\cal F$, hence $Fam(U)\contr_I Fam(V)$,
2886	implying [creation] in $\lin{{\cal F}}$. Since complete family-reductions can be
2887	viewed as reduction in $\cal F$ (by considering multi-steps as
2888	corresponding complete developments), [contribution] for $\contr_I$ follows
2889	immediately from [contribution] for $\contr$. Finally, [FFD] for
2890	$\lin{{\cal F}}$ follows immediately from \Lr{L.fam.compl.} for $\calF$.
2891	Hence $\lin{{\cal F}}$ is indeed a DFS as $\fami_I$ clearly
2892	contains the zig-zag relation. Note that $\lin{{\cal F}}$ is separable as

2894	clearly external). The axiom [initial] in $\lin{{\calF}}$ follows
2895	immediately from [initial] in $\calF$. If $P+U+V$ is a reduction in
2896	$\lin{{\calF}}$ such that $U$ creates $V$, then the redexes in $V$ are
2897	created along $U$ (when $P+U+V$ is considered as a reduction in $\calF$),
2898	i.e., $Fam(U)\contr Fam(V)$ in $\calF$, hence $Fam(U)\contr_I Fam(V)$,
2899	implying [creation] in $\lin{{\calF}}$. Since complete family-reductions can be
2900	viewed as reduction in $\calF$ (by considering multi-steps as
2901	corresponding complete developments), [contribution] for $\contr_I$ follows
2902	immediately from [contribution] for $\contr$. Finally, [FFD] for
2903	$\lin{{\calF}}$ follows immediately from \Lr{L.fam.compl.} for $\calF$.
2904	Hence $\lin{{\calF}}$ is indeed a DFS as $\fami_I$ clearly
2905	contains the zig-zag relation. Note that $\lin{{\calF}}$ is separable as


Nonmatching lines (File "atoe-tcsD.tex"; Line 2899; File "atoe-tcsJE.tex"; Line 2912)
2899	For any DFS ${\cal F}$, $\lin{{\cal F}}$ is an AZDFS.

2912	For any DFS ${\calF}$, $\lin{{\calF}}$ is an AZDFS.


*** EOF on both files at the same time ***
